\section{Teoria typów Per'a Matin-L{\"o}f'a} \label{sec:pml}
Teoria typów {\PerMartinLofDopelniacz} stanowi łącznik między matematyką i programowaniem. Może być wykorzystana jako konstruktywna podstawa matematyki \cite[rodział 3.4]{sep-mathematics-constructive} i specyfikacja zależnie typowanego języka programowania \cite{agdafoundation}.

Teoria typów {\PerMartinLofDopelniacz} jest systemem dedukcji opartym na dwóch typach osądów \cite{hottbook}:
\begin{center}
\medskip
\begin{tabular}{c l}
  Osąd & Znaczenie \\
  \hline
  $a : A$      & ``$a$ jest obiektem typu $A$''\\
  $a \equiv b : A$ & ``$a$ i $b$ są równoważnymi z definicji obiektami typu $A$''\\
\end{tabular}
\medskip
\end{center}

Osąd $a : A$ może być interpretowany w równoważności Curry’ego-Howarda \cite{howard} jako ``a jest dowodem hipotezy A''.

Należy odróżnić osąd $a \equiv b : A$ (równoważność z definicji) od typu \id[A]{x}{y}\footnote{Typ identycznościowy jest zdefiniowany w (\ref{subsec:typ-identycznosciowy})} (hipoteza równości dwóch obiektów). Na przykład: \id[\mathbb{N}]{13}{37} jest poprawnie zdefiniowanym typem który nie ma instancji (hipoteza bez dowodu), lecz osąd $13 \equiv 37 : \mathbb{N}$ jest błędny, nie może wystąpić nawet w hipotezie.

Poniżej zostają przedstawione podstawowe typy i reguły typowania dla nich.
%Najnowsza mi znana \cite{pmlnewest} i całkiem przystępne notatki G. Sambina \cite{pmlnotes} \\
%+ dobry opis przy okazji HOTT (ale bez aksjomatu k) \cite{hottbook}
%Teorie typów nie używają logiki pierwszego rzędu w swoich definicjach.
\subsection{Definicja typu}
Definicja typu na ogół składa się z:
\begin{enumerate}
\item reguł(y) formacji typu -- czyli sposobu formowania hipotezy w interpretacji Curry’ego-Howarda (na przykład: żeby skonstruować typ funkcji z $A$ do $B$ najpierw musi istnieć typ $A$ i $B$),
\item reguł(y) wprowadzenia typu (konstruktora) -- czyli sposobu konstruowania dowodu (na przykład: $\lambda$),
\item reguł(y) eliminacji -- czyli sposobu przekształcenia jednego dowodu w drugi (na przykład: aplikacja funkcji),
\item (opcjonalnie) reguł(y) unikalności -- czyli osądu równości dla instancji typu, nie zawsze wsytępuje.
\end{enumerate}

\subsection{Wszechświaty} \label{subsec:wszechswiaty}
Wszechświaty są typami typów (oznaczanymi \(\universe{}\) od ang. \emph{Universe} - wszechświat).
Na przykład, typ liczby $0$ to liczba naturalna (\( 0 : \nat \)), a typ typu \( \nat \) to \(\universe{0}\).
%Jaki jest typ \(\universe{0}\)?
Postuluje się istnienie hierarchii wszechświatów:
\[ \mathcal{U}_0 : \mathcal{U}_1 \qquad \mathcal{U}_1 : \mathcal{U}_2 
\qquad \cdots \qquad \mathcal{U}_{n} : \mathcal{U}_{n+1} \]
Indeksy wszechświatów są zewnętrzne dla teorii, tzn. indeksy nie są wartościami jakiegoś typu. Poniższy typ jest źle zdefiniowany:
\[ \Pi_{(i : Indeks)} \mathcal{U}_i \]
Wszechświaty są kumulatywne, tzn. elementy niższych wszechświatów są również elementami wyższych wszechświatów, np:
\[ \nat : \universe{0} \qquad  \nat : \universe{1} \] 

\subsubsection{Konieczność istnienia hierarchii wszechświatów}
W pierwszych wersjach teorii \cite{pmlfirst} zakładano że \( \mathcal{U} : \mathcal{U}\). W takiej teorii dało się udowodnić absurd (podlegała paradoksowi Girarda \cite{analysisofgirard}, teoriotypowemu odpowiednikowi paradoksu Russela).


%\subsection{Typ funkcji}
\subsection{Funkcje proste} \label{subsec:funkcje-proste}
Funcje są typem danym z góry, w przeciwieństwie do matematyki opartej na teorii mnogości, gdzie funkcje definiuje się na podstawie relacji.
\subsubsection{Reguła formacji}
Niech $A : \universe{i}$ i $B : \universe{i}$ będą typami, wtedy
\[A \rightarrow C : \universe{i}\]
jest typem funkcji z $A$ do $B$.

\subsubsection{Reguła wprowadzenia}
Funkcje z $A$ do $B$ wprowadza się $\lambda$-abstrakcją \(\left(\lambda x . \Phi \right)\) lub definiując ją wprost \(\left(f(x) :\equiv \Phi \right)\),
gdzie $\Phi$ może zawierać $x$. Musi zachodzić $\Phi : B$ przy założeniu że $x : A$ (bardziej formalny opis tworzy sie w oparciu o \href{https://pl.wikipedia.org/wiki/Dedukcja\_naturalna}{naturalną dedukcję}).

\subsubsection{Reguła eliminacji}
Regułą eliminacji dla funkcji jest aplikacja funkcji, tzn:
\[ \left(\lambda x . \Phi\right)(a) \equiv \Phi\prime \]
gdzie $\Phi\prime$ to $\Phi$ gdzie wszystkie wystąpienia $x$ zamieniono na $a$.
\subsubsection{Reguła unikalności}
Reguła unikalności dla funkcji mówi, że funkcja która aplikuje $f$ do swojego argumentu jest równa $f$: \[ f \equiv \lambda x . f(x) \]

\subsection{Funkcje zależne}
Funkcja zależna $\fnd{x:A}{B(x)}$ odpowiada klasycznemu \(\forall x \in A : x \in B\).
W teorii typów funkcje interpretuje się jako twierdzenia: argumenty funkcji to założenia a wartość zwracana to dowód. Funkcje proste (\ref{subsec:funkcje-proste}) nie wystarczają do opisania rzeczywistych twierdzeń, jak naprzykład twierdzenia \ref{thm:a-b=0}.
\subsubsection{Reguła formacji}
Jeśli $(A : \universe{i})$ jest typem, a $(B : A \rightarrow \universe{i})$ jest funckją prostą z $A$ do uniwersum typów, wtedy
\[\fnd{x : A} B(x) : \universe{i}\]
jest funkcją zależną. Typ zwracany przez funkcję zależy od typu wejściowego.
\subsubsection{Reguły wprowadzenia, eliminacji, unikalności}
Są analogiczne do reguł dla funkcji prostych.
\subsubsection{Dodatkowe uwagi}
Jeżeli w typie funkcji zależnej $\fnd{x:A}{B}$ typ zwracany nie zależy od wartości przyjmowanej przez funkcję, wtedy funkcja zależna jest równoważna funkcji prostej:
\[ \fnd{x:A}{B} \equiv A \rightarrow B \]

\subsection{Typy o wyliczonej, skończonej liczbie elementów}
Definiuje się typ jednostkowy \( \unit : \universe{0} \) którego jedynym elementem jest \( \ttu : \mathbf{1} \).
Definiuje się typ pusty służący jako absurd (\ref{subsec:absurd}), który nie ma żadnych elementów \( \emptytype : \universe{0}\).
Reguła eliminacji dla typu pustego opowiada \emph{Ex falso quodlibet}:
\[ rec_{\emptytype} : \fnd{C : \universe{i}}{\emptytype \rightarrow C} \]

\subsection{Typ identycznościowy} \label{subsec:typ-identycznosciowy}
Typy identycznościowe to rodzina typów odpowiadająca hipotezom, że dwie instancje tego samego typu są równe.
\subsubsection{Konstrukcja typu}
Niech:
\begin{align*}
  A &: \universe{i} \\
  a &: A \\
  b &: A
\end{align*}
wtedy \(Id(a,b) : \universe{i} \), zapisywane także jako \( {\idtype{A}{a}{b}}\). Należy zwrócić uwagę, że powyżej został zdefiniowany typ identycznościowy, a nie sposób konstrukcji typu. Innnymi słowy, \( \idtype{A}{a}{b} \) jest hipotezą, że $a$ i $b$ są równe, nie dowodem.
\subsubsection{Konstrukcja instancji}
Instancję typu identycznościowego (dowód) można skonstruować używając konstruktowa zwrotności (ang. \emph{reflexivity}). Dla każdego typu \(A : \universe{i}\) istnieje funkcja:
\[ refl : \Pi_{(x : A)}  \idtype{A}{x}{x} \]
\subsubsection{Reguła indukcyjna} \label{subsubsec:regula-indukcyjna}
Reguła indukcyjna typu identycznościowego mówi, że dla wyznaczonego \(x : A\) rodzina typów \(\lambda y.\idtype{A}{x}{y} \) może być generowana przez \(refl(x)\). Niech $C$ będzie rodziną typów, a $c$ przedstawicielem rodu dla \(refl(x) \):
\begin{align*}
  C &: \Pi_{(x,y:A)} (\idtype{A}{x}{y}) \to \universe{} \\
  c &: \Pi_{(x:A)} C(x,x,refl(x))  
\end{align*}
Reguła mówi, że istnieje funkcja \(f\), która z definicji jest równa $c(x)$ dla argumentu $refl(x)$:
\begin{align*}
  f& : \Pi_{(x,y:A)} \Pi_{(p:\idtype{A}{x}{y})} C(x,y,p) \\
  f&(x,x,refl(x)) \equiv c(x) 
\end{align*}
Na podstawie tej reguły pokazuje się że każda rodzina typów zachowuje równość.
Niech \(Q : A \rightarrow \universe{i} \) będzie rodziną typów.
Konstruuje się:
\begin{itemize}
\item \(C(x,y,p) \equiv   Q(x) \rightarrow Q(y) \quad\) - rodzinę typów,
\item \(c(x,x,refl(x)) \equiv \lambda q . q \quad\) - funkcję identycznościową w $Q(x)$ (bo \(q : Q(x) \)).
\end{itemize}
Zgodnie z regułą idukcyjną otrzymuje się funckję
\[ f : \fnd{x,y:A}{\fnd{p: \idtype{A}{x}{y}}{Q(x) \rightarrow Q(y)}} \]
taką, że
\[ f(x,x,refl(x)) \equiv \lambda q . q\]
Teoriomnogościowa interpretacja funckji $f$ jest następująca:
\[ x \in Q \land x = y \implies y \in Q  \]
To wydaje się oczywiste z teoriomnogościowego punktu widzenia, natomiast ta własność nie wynika z samej konstrukcji elementów typu indentycznościowego (\(refl\)), a z reguły indukcyjnej dla typu identycznościowego.

\subsubsection{Dodatkowe uwagi}
Reguła indukcyjna zdefiniowana w kilku punktach w  (\ref{subsubsec:regula-indukcyjna}) może być krócej zapisana jako\footnote{$J$ to zwyczajowa, spotykana w literaturze nazwa reguły indukcyjnej dla typu identycznościowego}:
\begin{align*}
  J &: \fnd{C: \fnd{x,y:A}{(\idtype{A}{x}{y}) \rightarrow \universe{i} }}  {\left( \fnd{x:A}{C(x,x,refl(x))}\right) \rightarrow \fnd{x,y:A}{\fnd{p:\idtype{A}{x}{y}}{C(x,y,p)}}} \\
  J &(C,c,x,x,refl(x)) \equiv c(x)
  \end{align*}
Powyżej podana reguła jest nazywana nieuziemioną, gdyż zastępuje się oba końce ścieżki przez nowy element $x$. Można zdefniować (i pokazać równoważność obydwu definicji \cite{hottbook}) uziemioną wersję reguły, w której jeden z końców ścieżki jest stały ($a$):
\begin{align*}
  J\prime &:  \fnd{a:A}{\fnd{C : \fnd{x:A}{(\idtype{A}{a}{x}) \rightarrow \universe{i}}}{C(a,refl(a)) \rightarrow \fnd{a:A}{\fnd{p:\idtype{A}{a}{x}}{C(x,p)}}}}\\
  J\prime&(a,C,c,a,refl(a)) \equiv c  
\end{align*}

\subsection{Pary zależne} \label{subsec:pary-zalezne}
Typ pary zależnej \(\deppair{x:A}{B(x)}\) odpowiada hipotezie:  \( \exists x \in A : x \in B \).
\subsubsection{Reguła formacji}
Jeśli $(A: \universe{i})$ oraz \(\left(B: A \rightarrow \universe{i}\right)\) to istnieje typ
\[ \deppair{x:A}{B(x)} \]

\subsubsection{Reguła wprowadzenia}
Jeżeli $x : A$ i $y : B(x)$ to
\[ (x,y) : \deppair{x:A}{B(x)}\]

\subsubsection{Reguła eliminacji}
Reguła eliminacji opiera się na podaniu funkcji zależnej. Niech \(\left(\deppair{x:A}{B(x)} : \universe{i}\right) \). Niech \(\left(C: \deppair{x:A}{B(x)} \rightarrow \universe{j}\right)\). Jeśli poda się funkcję
\[ g : \fnd{a:A}{\fnd{b:B(a)} C((a,b))}\]
to otrzyma się
\[ f : \fnd{p:\deppair{x:A}{B(x)}} {C(p)}\]
taką, że
\[ f((a,b)) \equiv g(a)(b) \]
Można to skrócić do pojedynczej definicji:
\begin{align*}
  %rec_\Sigma &:  \fnd{C: \universe{j}}{\left( \fnd{x:A} B(x) \rightarrow C\right) \rightarrow \left(\deppair{x:A}{B(x)}\right) \rightarrow C}\\
  %rec_\Sigma &(C,g,(a,b)) \equiv g(a)(b)
  ind_\Sigma &:  \fnd{C:\left(\deppair{x:A}{B(x)}\right) \rightarrow \universe{j}}{    \left( \fnd{x:A} {\fnd{y:B(x)}{C((x,y))}} \right) \rightarrow  \fnd{p: \deppair{x:A}{B(x)}}{C(p)}}\\
  ind_\Sigma &(C,g,(a,b)) \equiv g(a)(b)
\end{align*}


\subsubsection{Rzutowania}
 Reguła eliminacji pozwala skonstruować rzutowania, które pozwalają ``odzyskać'' wartości użyte do stworzenia pary
 \begin{align*}
   pr_1 &: \deppair{x:A}{B(x)} \rightarrow A \\
   pr_1&(p) =  ind_\Sigma (\lambda p . A, \lambda a . \lambda b . a,p)\\
   pr_2 &: \fnd{p:\deppair{x:A}{B(x)}}{ B(pr_1(p))}\\
   pr_2 &(p) = ind_\Sigma \left(\lambda p . B\left(pr_1(p)\right), \lambda a . \lambda b . b , p \right)
 \end{align*}

\subsubsection{Dodatkowe uwagi}
Jeżeli drugi element pary nie zależy od wartości pierwszego \(\left(\deppair{x:A}{B}\right)\), to wtedy mówi się o zwykłej (niezależnej) parze, odpowiadającej iloczynowi kartezjańskiemu. Taka para jest konstruktywistycznym odpowiednikiem koniunkcji.
\[ \deppair{x:A}{B} \equiv A \times B\]

%DOZRO: pisać o aksjomacie wyboru?

\subsection{Wspólnoty} \label{subsec:wspolnoty}
Typ wspólnot to konstruktywistyczny odpowiednik alternatywy
\subsubsection{Reguła formacji}
Jeżeli $A: \universe{i}$ i $B : \universe{i}$ są typami, to
\[ \sumtype{A}{B} : \universe{i}\]
\subsubsection{Reguły wprowadzenia}
Instancję typu wspólnot można uzyskać podając odpowiednio:
\begin{enumerate}
\item lewą stronę alternatywy : \(\suminl : A \rightarrow \sumtype{A}{B} \),
\item prawą stronę alternatywy : \(\suminr : B \rightarrow \sumtype{A}{B} \).
\end{enumerate}
\subsubsection{Reguła eliminacji}
Niech $\left( \sumtype{A}{B} : \universe{i} \right)$, jeśli $C : \sumtype{A}{B} \rightarrow \universe{j}$ i
\begin{align*}
  g_l &: \fnd{a:A}{C(\suminl(a))} \\
  g_r &: \fnd{b:B}{C(\suminr(b))} 
\end{align*}
to instnieje funkcja $f$ taka że:
\begin{align*}
  f &: \fnd{x: \sumtype{A}{B}}{C(x)} \\
  f&(\suminl(a)) \equiv g_l(a)\\
  f&(\suminr(b)) \equiv g_r(a)
\end{align*}
W wersji skróconej:
\begin{align*}
  ind_{\sumtype{A}{B}} &: \fnd{C: \sumtype{A}{B} \rightarrow \universe{j}}{
    \left( \fnd{a:A}{C\left(\suminl(a)\right)}   \right) \rightarrow
    \left( \fnd{b:B}{C\left(\suminl(b)\right)}   \right) \rightarrow
    \fnd{x:\sumtype{A}{B}}{C(x)}} \\
  ind_{\sumtype{A}{B}} &(C,g_l,g_r,\suminl(a)) \equiv g_l(a) \\
  ind_{\sumtype{A}{B}} &(C,g_l,g_r,\suminr(b)) \equiv g_r(b)
\end{align*}

\subsubsection{Dodatkowe uwagi}
Należy zwrócić uwagę że, dla typu $\sumtype{A}{A}$ nie jest prawdą że $\suminl(x) = \suminr(x)$ (nie da się skonstruować takiego dowodu). Dlatego typ boole'owski można implementować jako $\sumtype{\unit}{\unit}$, gdzie prawda odpowiada $\suminl$, a fałsz $\suminr$ (lub na odwrót).


\subsection{Typy indukcyjne: W-typy} \label{subsec:w-typy}
Od teorii typów używanej do odwzorowania matematyki klasycznej oczekuje się, że będzie w stanie odwzorować postawowe struktury matematyczne, jak na przykład liczby naturalne. Używając postulatów Peano, można zdefiniować liczby naturalne jako typ ``wbudowany'' w teorię.
Liczby naturalne (w postulatach Peano) są przykładem typu, który można zdefiniować podając klasę bazową (zero), oraz metodę konstrukcji nowych instancji na podstawie już istniejących (operacja następnika)\footnote{Typy o skończonej liczbie elementów (jak $\unit$) również są typami indukcyjnymi bez metody konstrukcji nowych elementów}. Takie typy nazywa się \emph{indukcyjnymi}. Mechanizm definiowania nowych typów indukcyjnych zawiera się w W-typach (od \emph{Well-founded trees}). Przykłady wykorzystania W-typów znajdują się w (\ref{subsec:tworzenie-nowych-typow}). Dokładniejszy opis W-typów znajduje się w \cite[rodział 5.3]{hottbook}.

\subsubsection{Reguła formacji}
Jeśli \((A : \universe{i})\) i \((B : A \rightarrow \universe{i})\) to
\[ \wtype{x:A}{B(x)} : \universe{i}\]
Ilość instancji typu $A$ określa ilość konstruktorów typu, ilość instancji $B(x)$ określa liczbę argumentów wymaganych przez konstruktor.

\subsubsection{Reguła wprowadzenia}
Jeżeli \((a : A)\) i \((y : B(a) \rightarrow \wtype{x:A}{B(x)})\) to
\[ \wsup(a,y) : \wtype{x:A}{B(x)} \]
Konieczność podania instancji \((y : B(a) \rightarrow \wtype{x:A}{B(x)})\) wydaje się pozornie sprzeczna, przykład jej wykorzystania znajduje się w (\ref{subsec:tworzenie-nowych-typow}).
\subsubsection{Reguła eliminacji}
Jeżeli poda się:
\begin{align*}
  C &: \wtype{x:A}{B(x)} \rightarrow \universe{j}\\
  d &: \fnd{a:A}{\fnd{u: B(a) \rightarrow \wtype{x:A}{B(x)}}{
      \left(\left(\fnd{y:B(a)}{C(u(y))}\right) \rightarrow C(\wsup(a,u))\right)
  }}
\end{align*}
to otrzyma się
\begin{align*}
  f &: \fnd{z:\wtype{x:A}{B(x)}}{C(z)}\\
  f &(\wsup(a,u)) = d(a,u,f \circ u)
\end{align*}


\subsection{Tworzenie nowych typów} \label{subsec:tworzenie-nowych-typow}
Poniżej przedstawiamy jak skonstruować typy $Bool$ i $\nat$ na podstawie wyżej wymienionych typów. %TU DOPISAĆ `List` jeśli dodam
\subsubsection{Typ boole'owski} \label{subsubsec:bool-konstr}
Typ $Bool$ zawierający dwie wartości : $true$ i $false$ można skonstruować jako:
\begin{align*}
  Bool &: \universe{0} \\
  Bool &\equiv \sumtype{\unit}{\unit} \\
  true &\equiv \suminl(\ttt) \\
  false &\equiv \suminr(\ttt)  \\
  if &: \fnd{C : \fnd{b : Bool}{\universe{j}}}{\left(C(true) \rightarrow C(false) \rightarrow \fnd{b: Bool}{C(b)} \right)} \\
  if &(C,t,f,b) = ind_{a+B}(C,\lambda x . C(true), \lambda x . C(false), b  ) 
\end{align*}
\subsubsection{Liczby naturalne} \label{subsubsec:nat-konstr}
Liczby naturalne w postulatach Peano definiuje się następująco:
\begin{align*}
  0 &: \nat \\
  suc &: \nat \rightarrow \nat
\end{align*}
Aby przełożyć to na W-typ potrzeba typu o takiej ilości instancji, ile konstruktorów liczb naturalnych, czyli dwóch (jak $Bool$).
Pierwszy konstruktor jest bezargumentowy, a zatem będzie reprezentowany przez $\emptytype$. Drugi konstruktor jest jednoargumentowy, będzie reprezentowany przez $\unit$.
\begin{align*}
  \nat &: \universe{0} \\
  \nat &\equiv \wtype{x:Bool}{if \left( \lambda x . \universe{0}, \emptytype, \unittype, x \right)} \\
  0 &\equiv \wsup(true, \lambda e . rec_{\emptytype}(\nat, e)) \\
  suc &\equiv \lambda pred . \wsup(false, \lambda t . pred)
\end{align*}
Zero konstruuje się używając reguły eliminacji dla typu pustego, czyli \emph{Ex falso quodlibet}; w ten sposób ``z niczego'' powstaje pierwsza liczba naturalna.

Operacja następnika podaje poprzednika do funckji $\wsup$. Mimo, iż pozornie poprzednik nie został zmieniony, to nie istnieje sposób, aby dowieść że \(\deppair{n:\nat}{\left( n = suc(n) \right)} \)

%\subsubsection{Listy}
%Listy powstają w analogiczny sposób tylko trochę inaczej xD
% dopisać na górze jakbym dorabiał
